\begin{tabbing}
pre{-}init{-}p2(${\it es}$;$i$;${\it ds}$;${\it init}$;$a$;$p$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=pre{-}init{-}p(${\it es}$; $i$; ${\it ds}$; ${\it init}$; $P$)\+
\\[0ex]\& @$i$ \=Precondition for $a$:Outcome($p$) is \+
\\[0ex]$P$:State(${\it ds}$)$\rightarrow$ $\mathbb{B}$
\-\\[0ex]\& ($\forall$$x$:Id. ($\uparrow$$x$ $\in$ dom(${\it ds}$)) $\Rightarrow$ @$i$ $x$ initially ${\it init}$($x$):${\it ds}$($x$))
\-
\end{tabbing}